1  /-
  2  Copyright (c) 2019 Jan-David Salchow. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
  5  
  6  Operator norm on the space of continuous linear maps
  7  
  8  Define the operator norm on the space of continuous linear maps between normed spaces, and prove
  9  its basic properties. In particular, show that this space is itself a normed space.
 10  -/
 11  
 12  import topology.metric_space.lipschitz analysis.normed_space.riesz_lemma
src         └─────────────────────────────┘ └───────────────────────────────┘
 13  import analysis.asymptotics
src         └──────────────────┘
 14  noncomputable theory
 15  open_locale classical
 16  
 17  set_option class.instance_max_depth 70
doc             └──────────────────────┘
 18  
 19  variables {𝕜 : Type*} {E : Type*} {F : Type*} {G : Type*}
 20  [normed_group E] [normed_group F] [normed_group G]
 21  
 22  open metric continuous_linear_map
 23  
 24  lemma exists_pos_bound_of_bound {f : E → F} (M : ℝ) (h : ∀x, ∥f x∥ ≤ M * ∥x∥) :
 25    ∃ N, 0 < N ∧ ∀x, ∥f x∥ ≤ N * ∥x∥ :=
 26  ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), λx, calc
id               └──────────┘ └─────────┘  └──────────┘        
src              └──────────┘ └─────────┘  └──────────┘
typ              └──────────┘ └┘└───────┘  └──────────┘        
 27    ∥f x∥ ≤ M * ∥x∥ : h x
id               
src              
typ              
 28    ... ≤ max M 1 * ∥x∥ : mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) ⟩
id           └─┘        └────────────────────────┘  └─────────┘       └─────────┘
src          └─┘          └────────────────────────┘  └─────────┘       └─────────┘
typ          └─┘        └────────────────────────┘  └─────────┘       └─────────┘
 29  
 30  section normed_field
 31  /- Most statements in this file require the field to be non-discrete, as this is necessary
 32  to deduce an inequality `∥f x∥ ≤ C ∥x∥` from the continuity of f. However, the other direction always
 33  holds. In this section, we just assume that `𝕜` is a normed field. In the remainder of the file,
 34  it will be non-discrete. -/
 35  
 36  variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] (f : E →ₗ[𝕜] F)
id              └──────────┘     └──────────┘       └──────────┘             └─┘ 
src             └──────────┘     └──────────┘       └──────────┘             └─┘ 
typ             └──────────┘     └──────────┘       └──────────┘             └─┘ 
doc             └──────────┘     └──────────┘       └──────────┘
 37  
 38  lemma linear_map.lipschitz_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
id                                                           
src                                                               
typ                                                          
 39    lipschitz_with (nnreal.of_real C) f :=
id     └────────────┘  └────────────┘   
src    └────────────┘  └────────────┘
typ    └────────────┘  └────────────┘   
doc    └────────────┘
 40  lipschitz_with.of_dist_le $ λ x y, by simpa [dist_eq_norm] using h (x - y)
id   └───────────────────────┘
src  └───────────────────────┘             └─────┘            └──────┘     └─
typ  └───────────────────────┘             └─────┘            └──────┘     └─
doc                                        └─────┘            └──────┘     └─
txt                                        └─────┘            └──────┘     └─
par                                        └─────┘            └──────┘     └─
pid                                                         └────┘     
 41  
src  
typ  
doc  
txt  
par  
pid  
 42  lemma linear_map.uniform_continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
 43    uniform_continuous f :=
 44  (f.lipschitz_of_bound C h).to_uniform_continuous
 45  
 46  lemma linear_map.continuous_of_bound (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
 47    continuous f :=
 48  (f.lipschitz_of_bound C h).to_continuous
 49  
 50  /-- Construct a continuous linear map from a linear map and a bound on this linear map.
 51  The fact that the norm of the continuous linear map is then controlled is given in
 52  `linear_map.mk_continuous_norm_le`. -/
 53  def linear_map.mk_continuous (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
 54  ⟨f, linear_map.continuous_of_bound f C h⟩
 55  
 56  /-- Construct a continuous linear map from a linear map and the existence of a bound on this linear
 57  map. If you have an explicit bound, use `linear_map.mk_continuous` instead, as a norm estimate will
 58  follow automatically in `linear_map.mk_continuous_norm_le`. -/
 59  def linear_map.mk_continuous_of_exists_bound (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
 60  ⟨f, let ⟨C, hC⟩ := h in linear_map.continuous_of_bound f C hC⟩
 61  
 62  @[simp, elim_cast] lemma linear_map.mk_continuous_coe (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
doc    └──┘  └───────┘
 63    ((f.mk_continuous C h) : E →ₗ[𝕜] F) = f := rfl
 64  
 65  @[simp] lemma linear_map.mk_continuous_apply (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
doc    └──┘
 66    f.mk_continuous C h x = f x := rfl
 67  
 68  @[simp, elim_cast] lemma linear_map.mk_continuous_of_exists_bound_coe (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) :
doc    └──┘  └───────┘
 69    ((f.mk_continuous_of_exists_bound h) : E →ₗ[𝕜] F) = f := rfl
 70  
 71  @[simp] lemma linear_map.mk_continuous_of_exists_bound_apply (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) (x : E) :
doc    └──┘
 72    f.mk_continuous_of_exists_bound h x = f x := rfl
 73  
 74  lemma linear_map.continuous_iff_is_closed_ker {f : E →ₗ[𝕜] 𝕜} :
 75    continuous f ↔ is_closed (f.ker : set E) :=
 76  begin
 77    -- the continuity of f obviously implies that its kernel is closed
 78    refine ⟨λh, (continuous_iff_is_closed.1 h) {0} (t1_space.t1 0), λh, _⟩,
src    └─────┘  └─┘                         └─┘ └┘ └─┘            └───┘ └───┘
typ    └─────┘  └─┘                         └─┘ └┘ └─┘            └───┘ └───┘
doc    └─────┘  └─┘                         └─┘ └┘ └─┘            └───┘ └───┘
txt    └─────┘  └─┘                         └─┘ └┘ └─┘            └───┘ └───┘
par    └─────┘  └─┘                         └─┘ └┘ └─┘            └───┘ └───┘
pid            └─┘                         └─┘ └┘ └─┘            └───┘ └───┘
 79    -- for the other direction, we assume that the kernel is closed
 80    by_cases hf : ∀x, x ∈ f.ker,
src    └───────┘  └─┘    
typ    └───────┘  └─┘    
doc    └───────┘  └─┘    
txt    └───────┘  └─┘    
par    └───────┘  └─┘    
pid              └─┘    
 81    { -- if `f = 0`, its continuity is obvious
 82      have : (f : E → 𝕜) = (λx, 0), by { ext x, simpa using hf x },
src      └─────┘  └─┘   └┘   └───┘       └───┘  └──────────┘   
typ      └─────┘  └─┘   └┘   └───┘       └───┘  └──────────┘   
doc      └─────┘  └─┘   └┘   └───┘       └───┘  └──────────┘   
txt      └─────┘  └─┘   └┘   └───┘       └───┘  └──────────┘   
par      └─────┘  └─┘   └┘   └───┘       └───┘  └──────────┘   
pid      └───┘└┘  └─┘   └┘   └───┘          └┘       └────┘   
 83      rw this,
src      └─┘
typ      └─┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
 84      exact continuous_const },
src      └────┘                
typ      └────┘                
doc      └────┘                
txt      └────┘                
par      └────┘                
pid                           
 85    { /- if `f` is not zero, we use an element `x₀ ∉ ker f` such that `∥x₀∥ ≤ 2 ∥x₀ - y∥` for all
 86      `y ∈ ker f`, given by Riesz's lemma, and prove that `2 ∥f x₀∥ / ∥x₀∥` gives a bound on the
st       └──────────────────────────────────────────────────────────────────────────────────────────
 87      operator norm of `f`. For this, start from an arbitrary `x` and note that
st   ──────────────────────────────────────────────────────────────────────────────
 88      `y = x₀ - (f x₀ / f x) x` belongs to the kernel of `f`. Applying the above inequality to `x₀`
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
 89      and `y` readily gives the conclusion. -/
st   ─────────────────────────────────────────────
 90      push_neg at hf,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid              └────┘
st   ─────────────────┘└─
 91      let r : ℝ := (2 : ℝ)⁻¹,
id                          └┘
src      └──────┘└──┘ └──┘ └┘
typ      └──────┘└──┘ └──┘ └┘
doc      └──────┘ └──┘ └──┘ 
txt      └──────┘ └──┘ └──┘ 
par      └──────┘ └──┘ └──┘ 
pid      └───┘└─┘ └──┘ └──┘ 
st   ─────────────────────────┘└─
 92      have : 0 ≤ r, by norm_num [r],
id                                
src      └───────┘      └────────┘ 
typ      └───────┘     └────────┘
doc      └───────┘       └────────┘ 
txt      └───────┘       └────────┘ 
par      └───────┘       └────────┘ 
pid      └───┘└──┘               └┘ 
st   ───────────────┘                 └─
 93      have : r < 1, by norm_num [r],
id                                
src      └─────┘ └┘     └────────┘ 
typ      └─────┘└┘     └────────┘
doc      └─────┘  └┘     └────────┘ 
txt      └─────┘  └┘     └────────┘ 
par      └─────┘  └┘     └────────┘ 
pid      └───┘└┘               └┘ 
st   ───────────────┘                 └─
 94      obtain ⟨x₀, x₀ker, h₀⟩ : ∃ (x₀ : E), x₀ ∉ f.ker ∧ ∀ y ∈ linear_map.ker f, r * ∥x₀∥ ≤ ∥x₀ - y∥,
id                                              └───┘         └────────────┘              
src      └───────────────────────┘└─────┘    └───┘  └───┘└────────────┘         
typ      └───────────────────────┘└─────┘   └───┘  └───┘└────────────┘       
doc      └───────────────────────┘ └─────┘     └───┘  └───┘└────────────┘             
txt      └───────────────────────┘ └─────┘            └───┘                           
par      └───────────────────────┘ └─────┘            └───┘                           
pid            └─────────────────┘ └─────┘            └───┘                           
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
 95        from riesz_lemma h hf this,
id              └─────────┘  └┘ └──┘
src        └───┘└─────────┘   
typ        └───┘└─────────┘└┘└──┘
doc        └───┘└─────────┘   
txt        └───┘              
par        └───┘              
pid        └───┘              
st   ───────────────────────────────┘└─
 96      have : x₀ ≠ 0,
id              └┘ 
src      └─────┘  └┘
typ      └─────┘└┘└┘
doc      └─────┘   └┘
txt      └─────┘   └┘
par      └─────┘   └┘
pid      └───┘└┘   
st   ────────────────┘└─
 97      { assume h,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
 98        have : x₀ ∈ f.ker, by { rw h, exact (linear_map.ker f).zero },
id                └┘   └───┘                   └────────────┘ 
src        └─────┘   └───┘       └─┘   └────┘ └────────────┘ └─────┘
typ        └─────┘└┘ └───┘       └─┘  └────┘ └────────────┘└─────┘
doc        └─────┘   └───┘       └─┘   └────┘ └────────────┘ └─────┘
txt        └─────┘               └─┘   └────┘                └─────┘
par        └─────┘               └─┘   └────┘                └─────┘
pid        └───┘└┘                                         └───┘└┘
st   ──────────────────────┘     └───┘└──────────────────────────────┘└┘
 99        exact x₀ker this },
id               └───┘ └──┘
src        └────┘         
typ        └────┘└───┘└──┘
doc        └────┘         
txt        └────┘         
par        └────┘         
pid                      
st   ──────────────────────┘└┘
100      have rx₀_ne_zero : r * ∥x₀∥ ≠ 0, by { simp [norm_eq_zero, this], norm_num },
id                              └┘                  └──────────┘  └──┘
src      └─────────────────┘       └┘       └────┘└──────────┘└┘      └───────┘
typ      └─────────────────┘  └┘  └┘       └────┘└──────────┘└┘└──┘  └───────┘
doc      └─────────────────┘       └┘       └────┘            └┘      └───────┘
txt      └─────────────────┘       └┘       └────┘            └┘      └───────┘
par      └─────────────────┘       └┘       └────┘            └┘      └───────┘
pid      └──────────────┘└─┘                              └┘              
st   ──────────────────────────────────┘     └────────────────────────┘└─────────┘└┘
101      have : ∀x, ∥f x∥ ≤ (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥,
id                                             └┘
src      └─────┘                  └┘      └┘ 
typ      └─────┘                 └┘  └┘ └┘ 
doc      └─────┘                  └┘      └┘ 
txt      └─────┘                  └┘      └┘ 
par      └─────┘                  └┘      └┘ 
pid      └───┘└┘                  └┘      └┘ 
st   ─────────────────────────────────────────────────────┘└─
102      { assume x,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
103        by_cases hx : f x = 0,
id                        
src        └───────┘  └─┘   └┘
typ        └───────┘  └─┘ └┘
doc        └───────┘  └─┘   └┘
txt        └───────┘  └─┘   └┘
par        └───────┘  └─┘   └┘
pid                  └─┘   
st   ──────────────────────────┘└─
104        { rw [hx, norm_zero],
id               └┘  └───────┘
src          └──┘  └┘└───────┘
typ          └──┘└┘└┘└───────┘
doc          └──┘  └┘         
txt          └──┘  └┘         
par          └──┘  └┘         
pid            └┘  └┘         
st   ───────┘└────┘└─────────┘└──
105          apply_rules [mul_nonneg', norm_nonneg, inv_nonneg.2, norm_nonneg] },
id                        └─────────┘  └─────────┘  └────────┘    └─────────┘
src          └───────────┘└─────────┘└┘└─────────┘└┘└────────┘└──┘└─────────┘└┘
typ          └───────────┘└─────────┘└┘└─────────┘└┘└────────┘└──┘└─────────┘└┘
doc          └───────────┘           └┘           └┘          └──┘           └┘
txt          └───────────┘           └┘           └┘          └──┘           └┘
par          └───────────┘           └┘           └┘          └──┘           └┘
pid                     └┘           └┘           └┘          └──┘           
st   ─────────────────────────────────────────────────────────────────────────┘└┘
106        { let y := x₀ - (f x₀ * (f x)⁻¹ ) • x,
id                            └┘             
src          └───────┘             └─┘
typ          └───────┘     └┘     └─┘
doc          └───────┘             └─┘ 
txt          └───────┘             └─┘ 
par          └───────┘             └─┘ 
pid          └───┘└─┘             └─┘ 
st   ──────────────────────────────────────────┘└─
107          have fy_zero : f y = 0, by calc
id                                    └──┘
src          └─────────────┘   └┘     └──┘
typ          └─────────────┘ └┘     └──┘
doc          └─────────────┘   └┘     └──┘
txt          └─────────────┘   └┘
par          └─────────────┘   └┘
pid          └──────────┘└─┘   
st   ─────────────────────────────┘     └──┘
108            f y = f x₀ - (f x₀ * (f x)⁻¹ ) * f x :
id                            └┘                
typ                           └┘                
109              by { dsimp [y], rw [f.map_add, f.map_neg, f.map_smul], refl }
id                           
src                   └─────┘   └──┘         └┘         └┘            └───┘
typ                   └─────┘  └──┘└───────┘└┘└───────┘└┘└────────┘  └───┘
doc                   └─────┘   └──┘         └┘         └┘            └───┘
txt                   └─────┘   └──┘         └┘         └┘            └───┘
par                   └─────┘   └──┘         └┘         └┘            └───┘
pid                             └┘         └┘         └┘                
st                 └──────────┘└─────────────┘└─────────┘└──────────┘└──────┘└┘
110            ... = 0 :
111              by { rw [mul_assoc, inv_mul_cancel hx, mul_one, sub_eq_zero_of_eq], refl },
id                        └───────┘  └────────────┘ └┘  └─────┘  └───────────────┘
src                   └──┘└───────┘└┘└────────────┘  └┘└─────┘└┘└───────────────┘  └───┘
typ                   └──┘└───────┘└┘└────────────┘└┘└┘└─────┘└┘└───────────────┘  └───┘
doc                   └──┘         └┘                └┘       └┘                   └───┘
txt                   └──┘         └┘                └┘       └┘                   └───┘
par                   └──┘         └┘                └┘       └┘                   └───┘
pid                     └┘         └┘                └┘       └┘                       
st                 └──────────────┘└─────────────────┘└───────┘└─────────────────┘└──────┘└┘
112          have A : r * ∥x₀∥ ≤ ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥, from calc
id                                 └┘              
src          └───────┘                         └───┘    
typ          └───────┘        └┘            └───┘    
doc          └───────┘                         └───┘    
txt          └───────┘                         └───┘    
par          └───────┘                         └───┘    
pid          └────┘└─┘                         └───┘    
st   ─────────────────────────────────────────────────┘└───────────
113            r * ∥x₀∥ ≤ ∥x₀ - y∥ : h₀ _ (linear_map.mem_ker.2 fy_zero)
id                        └┘       └┘    └────────────────┘   └─────┘
src  ─────────┘             └─┘  └─┘ └────────────────┘└─┘       └─
typ  ─────────┘       └┘  └─┘└┘└─┘ └────────────────┘└─┘└─────┘└─
doc  ─────────┘             └─┘  └─┘                   └─┘       └─
txt  ─────────┘             └─┘  └─┘                   └─┘       └─
par  ─────────┘             └─┘  └─┘                   └─┘       └─
pid  ─────────┘             └─┘  └─┘                   └─┘       └─
st   ────────────────────────────────────────────────────────────────────
114            ... = ∥(f x₀ * (f x)⁻¹ ) • x∥ : by { dsimp [y], congr, abel }
id                                                         
src  ─────────────┘            └─┘   └─┘  └─┘└─────┘ └┘└───┘└┘└───┘└─
typ  ─────────────┘            └─┘   └─┘  └─┘└─────┘└┘└───┘└┘└───┘└─
doc  ─────────────┘            └─┘   └─┘  └─┘└─────┘ └┘     └┘└───┘└─
txt  ─────────────┘            └─┘   └─┘  └─┘└─────┘ └┘└───┘└┘└───┘└─
par  ─────────────┘            └─┘   └─┘  └─┘└─────┘ └┘└───┘└┘└───┘└─
pid  ─────────────┘            └─┘   └─┘  └────────┘ └────────────────
st   ───────────────────────────────────────────┘└──────────┘└─────┘└─────┘
115            ... = ∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥ :
id                                      
src  ─────────────┘                 └──
typ  ─────────────┘               └──
doc  ─────────────┘                 └──
txt  ─────────────┘                 └──
par  ─────────────┘                 └──
pid  ─────────────┘                 └──
st   ─────────────────────────────────────────
116              by rw [norm_smul, normed_field.norm_mul, normed_field.norm_inv],
id                      └───────┘  └───────────────────┘  └───────────────────┘
src  ───────────┘  └──┘└───────┘└┘└───────────────────┘└┘└───────────────────┘
typ  ───────────┘  └──┘└───────┘└┘└───────────────────┘└┘└───────────────────┘
doc  ───────────┘  └──┘         └┘                     └┘                     
txt  ───────────┘  └──┘         └┘                     └┘                     
par  ───────────┘  └──┘         └┘                     └┘                     
pid  ───────────┘  └───┘         └┘                     └┘                     
st   ─────────────┘└────────────┘└─────────────────────┘└─────────────────────┘└─
117          calc
id           └──┘
src          └──┘
typ          └──┘
doc          └──┘
st   ─────────────
118            ∥f x∥ = (r * ∥x₀∥)⁻¹ * (r * ∥x₀∥) * ∥f x∥ : by rwa [inv_mul_cancel, one_mul]
id                                         └┘                   └────────────┘  └─────┘
src                                                           └───┘└────────────┘└┘└─────┘└─
typ                                        └┘              └───┘└────────────┘└┘└─────┘└─
doc                                                           └───┘              └┘       └─
txt                                                           └───┘              └┘       └─
par                                                           └───┘              └┘       └─
pid                                                              └┘              └┘       
st   ───────────────────────────────────────────────────────┘└──────────────────┘└───────┘
119            ... ≤ (r * ∥x₀∥)⁻¹ * (∥f x₀∥ * ∥f x∥⁻¹ * ∥x∥) * ∥f x∥ : begin
src  ─────────┘
typ  ─────────┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ─────────┘
st   ─────────┘└──────────────────────────────────────────────────────┘└─────
120              apply mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left A _) (norm_nonneg _),
id                     └────────────────────────┘  └───────────────────────┘      └─────────┘
src              └────┘└────────────────────────┘ └───────────────────────┘ └──┘ └─────────┘└─┘
typ              └────┘└────────────────────────┘ └───────────────────────┘└──┘ └─────────┘└─┘
doc              └────┘                                                     └──┘            └─┘
txt              └────┘                                                     └──┘            └─┘
par              └────┘                                                     └──┘            └─┘
pid                                                                        └──┘            └─┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
121              exact inv_nonneg.2 (mul_nonneg' (by norm_num) (norm_nonneg _))
id                     └────────┘    └─────────┘                └─────────┘
src              └────┘└────────┘└─┘ └─────────┘   └──────┘└┘ └─────────┘└────
typ              └────┘└────────┘└─┘ └─────────┘   └──────┘└┘ └─────────┘└────
doc              └────┘          └─┘               └──────┘└┘            └────
txt              └────┘          └─┘               └──────┘└┘            └────
par              └────┘          └─┘               └──────┘└┘            └────
pid                             └─┘               └─────────┘            └──┘
st   ──────────────────────────────────────────────┘└───────┘└──────────────────
122            end
src  ─────────┘
typ  ─────────┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ─────────┘
st   ─────────┘└─┘
123            ... = (∥f x∥ ⁻¹ * ∥f x∥) * (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ : by ring
src                                                                            └────
typ                                                                            └────
doc                                                                            └────
txt                                                                            └────
par                                                                            └────
pid                                                                                
st   ────────────────────────────────────────────────────────────────────────┘└─────
124            ... = (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥ :
src  ─────────┘
typ  ─────────┘
doc  ─────────┘
txt  ─────────┘
par  ─────────┘
pid  ─────────┘
st   ─────────┘└───────────────────────────────────────
125              by { rw [inv_mul_cancel, one_mul], simp [norm_eq_zero, hx] } } },
id                        └────────────┘  └─────┘         └──────────┘  └┘
src                   └──┘└────────────┘└┘└─────┘  └────┘└──────────┘└┘  └┘
typ                   └──┘└────────────┘└┘└─────┘  └────┘└──────────┘└┘└┘└┘
doc                   └──┘              └┘         └────┘            └┘  └┘
txt                   └──┘              └┘         └────┘            └┘  └┘
par                   └──┘              └┘         └────┘            └┘  └┘
pid                     └┘              └┘                         └┘  
st   ─────────────┘└───────────────────┘└───────┘└─────────────────────────┘└────┘
126      exact linear_map.continuous_of_bound f _ this }
id             └────────────────────────────┘    └──┘
src      └────┘└────────────────────────────┘ └─┘    
typ      └────┘└────────────────────────────┘└─┘└──┘
doc      └────┘                               └─┘    
txt      └────┘                               └─┘    
par      └────┘                               └─┘    
pid                                          └─┘    
st   ─────────────────────────────────────────────────┘└─
127  end
st   ──┘
128  
129  end normed_field
130  
131  variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G]
id             └──────────────────────┘     └──────────┘       └──────────┘       └──────────┘
src             └──────────────────────┘     └──────────┘       └──────────┘       └──────────┘
typ            └──────────────────────┘     └──────────┘       └──────────┘       └──────────┘
doc             └──────────────────────┘     └──────────┘       └──────────┘       └──────────┘
132  (c : 𝕜) (f g : E →L[𝕜] F) (h : F →L[𝕜] G) (x y z : E)
id                    └─┘            └─┘ 
src                   └─┘            └─┘ 
typ                   └─┘            └─┘ 
doc                   └─┘            └─┘ 
133  include 𝕜
134  
135  /-- A continuous linear map between normed spaces is bounded when the field is nondiscrete.
136  The continuity ensures boundedness on a ball of some radius `δ`. The nondiscreteness is then
137  used to rescale any element into an element of norm in `[δ/C, δ]`, whose image has a controlled norm.
138  The norm control for the original element follows by rescaling. -/
139  lemma linear_map.bound_of_continuous (f : E →ₗ[𝕜] F) (hf : continuous f) :
id                                              └─┘         └────────┘ 
src                                              └─┘           └────────┘
typ                                             └─┘         └────────┘ 
doc                                                             └────────┘
140    ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
id                          
src                                
typ                         
141  begin
st   └─────
142    have : continuous_at f 0 := continuous_iff_continuous_at.1 hf _,
id            └───────────┘       └──────────────────────────┘   └┘
src    └─────┘└───────────┘ └────┘└──────────────────────────┘└─┘  └┘
typ    └─────┘└───────────┘└────┘└──────────────────────────┘└─┘└┘└┘
doc    └─────┘└───────────┘ └────┘                            └─┘  └┘
txt    └─────┘              └────┘                            └─┘  └┘
par    └─────┘              └────┘                            └─┘  └┘
pid    └───┘└┘              └───┘                            └─┘  └┘
st   ────────────────────────────────────────────────────────────────┘└─
143    rcases metric.tendsto_nhds_nhds.1 this 1 zero_lt_one with ⟨ε, ε_pos, hε⟩,
id            └──────────────────────┘   └──┘   └─────────┘
src    └─────┘└──────────────────────┘└─┘    └─┘└─────────┘└──────────────────┘
typ    └─────┘└──────────────────────┘└─┘└──┘└─┘└─────────┘└──────────────────┘
doc    └─────┘                        └─┘    └─┘           └──────────────────┘
txt    └─────┘                        └─┘    └─┘           └──────────────────┘
par    └─────┘                        └─┘    └─┘           └──────────────────┘
pid                                  └─┘    └─┘           └──────────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
144    let δ := ε/2,
id              
src    └───────┘ 
typ    └───────┘
doc    └───────┘  
txt    └───────┘  
par    └───────┘  
pid    └───┘└─┘  
st   ─────────────┘└─
145    have δ_pos : δ > 0 := half_pos ε_pos,
id                         └──────┘ └───┘
src    └───────────┘ └────┘└──────┘
typ    └───────────┘└────┘└──────┘└───┘
doc    └───────────┘  └────┘        
txt    └───────────┘  └────┘        
par    └───────────┘  └────┘        
pid    └────────┘└─┘  └───┘        
st   ─────────────────────────────────────┘└─
146    have H : ∀{a}, ∥a∥ ≤ δ → ∥f a∥ ≤ 1,
id                           
src    └───────┘ └─┘         └┘
typ    └───────┘ └─┘       └┘
doc    └───────┘ └─┘            └┘
txt    └───────┘ └─┘            └┘
par    └───────┘ └─┘            └┘
pid    └────┘└─┘ └─┘            
st   ───────────────────────────────────┘└─
147    { assume a ha,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
148      have : dist (f a) (f 0) ≤ 1,
id              └──┘       
src      └─────┘└──┘   └┘  └──┘ └┘
typ      └─────┘└──┘  └┘ └──┘ └┘
doc      └─────┘       └┘  └──┘ └┘
txt      └─────┘       └┘  └──┘ └┘
par      └─────┘       └┘  └──┘ └┘
pid      └───┘└┘       └┘  └──┘ 
st   ──────────────────────────────┘└─
149      { apply le_of_lt (hε _),
id               └──────┘  └┘
src        └────┘└──────┘   └─┘
typ        └────┘└──────┘ └┘└─┘
doc        └────┘           └─┘
txt        └────┘           └─┘
par        └────┘           └─┘
pid                        └─┘
st   ─────┘└───────────────────┘└─
150        rw [dist_eq_norm, sub_zero],
id             └──────────┘  └──────┘
src        └──┘└──────────┘└┘└──────┘
typ        └──┘└──────────┘└┘└──────┘
doc        └──┘            └┘        
txt        └──┘            └┘        
par        └──┘            └┘        
pid          └┘            └┘        
st   ─────────────────────┘└────────┘└──
151        exact lt_of_le_of_lt ha (half_lt_self ε_pos) },
id               └────────────┘ └┘  └──────────┘ └───┘
src        └────┘└────────────┘   └──────────┘     └┘
typ        └────┘└────────────┘└┘ └──────────┘└───┘└┘
doc        └────┘                                  └┘
txt        └────┘                                  └┘
par        └────┘                                  └┘
pid                                               
st   ──────────────────────────────────────────────────┘└┘
152      simpa using this },
id                   └──┘
src      └──────────┘    
typ      └──────────┘└──┘
doc      └──────────┘    
txt      └──────────┘    
par      └──────────┘    
pid           └────┘    
st   ────────────────────┘└┘
153    rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
id            └─────────────────────────────┘ 
src    └─────┘└─────────────────────────────┘ └───────────┘
typ    └─────┘└─────────────────────────────┘└───────────┘
doc    └─────┘                                └───────────┘
txt    └─────┘                                └───────────┘
par    └─────┘                                └───────────┘
pid                                          └───────────┘
st   ──────────────────────────────────────────────────────┘└─
154    refine ⟨δ⁻¹ * ∥c∥, mul_pos (inv_pos δ_pos) (lt_trans zero_lt_one hc), (λx, _)⟩,
id             └┘      └─────┘  └─────┘ └───┘   └──────┘ └─────────┘ └┘
src    └─────┘  └┘   └┘└─────┘ └─────┘     └┘ └──────┘└─────────┘  └─┘  └────┘
typ    └─────┘ └┘  └┘└─────┘ └─────┘└───┘└┘ └──────┘└─────────┘└┘└─┘  └────┘
doc    └─────┘        └┘                    └┘                      └─┘  └────┘
txt    └─────┘        └┘                    └┘                      └─┘  └────┘
par    └─────┘        └┘                    └┘                      └─┘  └────┘
pid                  └┘                    └┘                      └─┘  └────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
155    by_cases h : x = 0,
id                   
src    └───────┘ └─┘ └┘
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  └┘
txt    └───────┘ └─┘  └┘
par    └───────┘ └─┘  └┘
pid             └─┘  
st   ───────────────────┘└─
156    { simp only [h, norm_zero, mul_zero, linear_map.map_zero] },
id                    └───────┘  └──────┘  └─────────────────┘
src      └─────────┘ └┘└───────┘└┘└──────┘└┘└─────────────────┘└┘
typ      └─────────┘└┘└───────┘└┘└──────┘└┘└─────────────────┘└┘
doc      └─────────┘ └┘         └┘        └┘                   └┘
txt      └─────────┘ └┘         └┘        └┘                   └┘
par      └─────────┘ └┘         └┘        └┘                   └┘
pid          └──┘└┘ └┘         └┘        └┘                   
st   ───┘└──────────────────────────────────────────────────────┘└┘
157    { rcases rescale_to_shell hc δ_pos h with ⟨d, hd, dxle, ledx, dinv⟩,
id              └──────────────┘ └┘ └───┘ 
src      └─────┘└──────────────┘        └─────────────────────────────┘
typ      └─────┘└──────────────┘└┘└───┘└─────────────────────────────┘
doc      └─────┘└──────────────┘        └─────────────────────────────┘
txt      └─────┘                        └─────────────────────────────┘
par      └─────┘                        └─────────────────────────────┘
pid                                    └─────────────────────────────┘
st   ────────────────────────────────────────────────────────────────────┘└─
158      calc ∥f x∥
id       └──┘
src      └──┘
typ      └──┘
doc      └──┘
st   ───────────────
159        = ∥f ((d⁻¹ * d) • x)∥ : by rwa [inv_mul_cancel, one_smul]
id                                      └────────────┘  └──────┘
src                                   └───┘└────────────┘└┘└──────┘└─
typ                                └───┘└────────────┘└┘└──────┘└─
doc                                   └───┘              └┘        └─
txt                                   └───┘              └┘        └─
par                                   └───┘              └┘        └─
pid                                      └┘              └┘        
st   ───────────────────────────────┘└──────────────────┘└────────┘
160        ... = ∥d∥⁻¹ * ∥f (d • x)∥ :
id                             
src  ─────┘                    
typ  ─────┘                    
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└───────────────────────────
161          by rw [mul_smul, linear_map.map_smul, norm_smul, normed_field.norm_inv]
id                  └──────┘  └─────────────────┘  └───────┘  └───────────────────┘
src             └──┘└──────┘└┘└─────────────────┘└┘└───────┘└┘└───────────────────┘└─
typ             └──┘└──────┘└┘└─────────────────┘└┘└───────┘└┘└───────────────────┘└─
doc             └──┘        └┘                   └┘         └┘                     └─
txt             └──┘        └┘                   └┘         └┘                     └─
par             └──┘        └┘                   └┘         └┘                     └─
pid               └┘        └┘                   └┘         └┘                     
st   ─────────┘└───────────┘└───────────────────┘└─────────┘└─────────────────────┘
162        ... ≤ ∥d∥⁻¹ * 1 :
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└─────────────────
163          mul_le_mul_of_nonneg_left (H dxle) (by { rw ← normed_field.norm_inv, exact norm_nonneg _ })
id           └───────────────────────┘   └──┘             └───────────────────┘        └─────────┘
src          └───────────────────────┘                └───┘└───────────────────┘  └────┘└─────────┘└─┘
typ          └───────────────────────┘   └──┘        └───┘└───────────────────┘  └────┘└─────────┘└─┘
doc                                                   └───┘                       └────┘           └─┘
txt                                                   └───┘                       └────┘           └─┘
par                                                   └───┘                       └────┘           └─┘
pid                                                     └─┘                                       └┘
st   ─────────────────────────────────────────────┘└───────────────────────────┘└────────────────────┘└┘
164        ... ≤ δ⁻¹ * ∥c∥ * ∥x∥ : by { rw mul_one, exact dinv } }
id                                       └─────┘        └──┘
src                                     └─┘└─────┘  └────┘    
typ                                   └─┘└─────┘  └────┘└──┘
doc                                     └─┘         └────┘    
txt                                     └─┘         └────┘    
par                                     └─┘         └────┘    
pid                                                         
st   ───────────────────────────────┘└───────────┘└───────────┘└───
165  end
st   ──┘
166  
167  namespace continuous_linear_map
168  
169  theorem bound : ∃ C, 0 < C ∧ (∀ x : E, ∥f x∥ ≤ C * ∥x∥) :=
id                                        
src                                              
typ                                       
170  f.to_linear_map.bound_of_continuous f.2
id   └────────────┘└──────────────────┘ 
src   └────────────┘└──────────────────┘  
typ  └────────────┘└──────────────────┘ 
doc                 └──────────────────┘
171  
172  section
173  open asymptotics filter
174  
175  theorem is_O_id (l : filter E) : is_O f (λ x, x) l :=
id                        └────┘     └──┘         
src                       └────┘      └──┘
typ                       └────┘     └──┘         
doc                                   └──┘
176  let ⟨M, hMp, hM⟩ := f.bound in is_O_of_le' l hM
id   └─┘          └┘     └────┘    └─────────┘ 
src                       └────┘    └─────────┘
typ  └─┘          └┘     └────┘    └─────────┘ 
177  
178  theorem is_O_comp {E : Type*} (g : F →L[𝕜] G) (f : E → F) (l : filter E) :
id                                       └─┘                  └────┘ 
src                                       └─┘                      └────┘
typ                                      └─┘                  └────┘ 
doc                                       └─┘ 
179    is_O (λ x', g (f x')) f l :=
id     └──┘    └┘     └┘    
src    └──┘
typ    └──┘    └┘     └┘    
doc    └──┘
180  (g.is_O_id ⊤).comp_tendsto lattice.le_top
id    └──────┘  └──────────┘  └────────────┘
src    └──────┘  └──────────┘  └────────────┘
typ   └──────┘  └──────────┘  └────────────┘
181  
182  theorem is_O_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
id                          └─┘        └────┘        
src                          └─┘          └────┘
typ                         └─┘        └────┘        
doc                          └─┘ 
183    is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
id     └──┘    └┘    └┘        └┘  └┘    
src    └──┘                             
typ    └──┘    └┘    └┘        └┘  └┘    
doc    └──┘
184  f.is_O_comp _ l
id   └────────┘   
src   └────────┘
typ  └────────┘   
185  
186  end
187  
188  section op_norm
189  open set real
190  
191  set_option class.instance_max_depth 100
doc             └──────────────────────┘
192  
193  /-- The operator norm of a continuous linear map is the inf of all its bounds. -/
194  def op_norm := Inf { c | c ≥ 0 ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ }
id                  └─┘                   
src                 └─┘                          
typ                 └─┘                   
195  instance has_op_norm : has_norm (E →L[𝕜] F) := ⟨op_norm⟩
id                          └──────┘   └─┘       └─────┘
src                         └──────┘    └─┘         └─────┘
typ                         └──────┘   └─┘       └─────┘
doc                         └──────┘    └─┘         └─────┘
196  
197  -- So that invocations of `real.Inf_le` make sense: we show that the set of
198  -- bounds is nonempty and bounded below.
199  lemma bounds_nonempty {f : E →L[𝕜] F} :
id                               └─┘ 
src                               └─┘ 
typ                              └─┘ 
doc                               └─┘ 
200    ∃ c, c ∈ { c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
id                           
src                                   
typ                          
201  let ⟨M, hMp, hMb⟩ := f.bound in ⟨M, le_of_lt hMp, hMb⟩
id   └─┘    └─┘  └─┘     └────┘        └──────┘
src                        └────┘        └──────┘
typ  └─┘    └─┘  └─┘     └────┘        └──────┘
202  
203  lemma bounds_bdd_below {f : E →L[𝕜] F} :
id                                └─┘ 
src                                └─┘ 
typ                               └─┘ 
doc                                └─┘ 
204    bdd_below { c | 0 ≤ c ∧ ∀ x, ∥f x∥ ≤ c * ∥x∥ } :=
id     └───────┘                   
src    └───────┘                          
typ    └───────┘                   
doc    └───────┘
205  ⟨0, λ _ ⟨hn, _⟩, hn⟩
id          └┘
typ         └┘
206  
207  lemma op_norm_nonneg : 0 ≤ ∥f∥ :=
id                             
src                             
typ                            
208  lb_le_Inf _ bounds_nonempty (λ _ ⟨hx, _⟩, hx)
id   └───────┘   └─────────────┘     └┘
src  └───────┘   └─────────────┘
typ  └───────┘   └─────────────┘     └┘
209  
210  /-- The fundamental property of the operator norm: `∥f x∥ ≤ ∥f∥ * ∥x∥`. -/
211  theorem le_op_norm : ∥f x∥ ≤ ∥f∥ * ∥x∥ :=
id                             
src                                
typ                            
212  classical.by_cases
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
213    (λ heq : x = 0, by { rw heq, simp })
id                           └─┘
src                        └─┘└─┘  └───┘
typ                       └─┘└─┘  └───┘
doc                         └─┘     └───┘
txt                         └─┘     └───┘
par                         └─┘     └───┘
pid                                    
st                       └───────┘└─────┘└┘
214    (λ hne, have hlt : 0 < ∥x∥, from (norm_pos_iff _).2 hne,
id        └─┘                        └──────────┘     └─┘
src                                   └──────────┘   
typ       └─┘                        └──────────┘     └─┘
215      le_mul_of_div_le hlt ((le_Inf _ bounds_nonempty bounds_bdd_below).2
id       └──────────────┘ └─┘   └────┘   └─────────────┘ └──────────────┘ 
src      └──────────────┘       └────┘   └─────────────┘ └──────────────┘ 
typ      └──────────────┘ └─┘   └────┘   └─────────────┘ └──────────────┘ 
216      (λ c ⟨_, hc⟩, div_le_of_le_mul hlt (by { rw mul_comm, apply hc }))))
id                   └──────────────┘ └─┘          └──────┘
src                    └──────────────┘           └─┘└──────┘  └────┘  
typ                  └──────────────┘ └─┘       └─┘└──────┘  └────┘  
doc                                               └─┘          └────┘  
txt                                               └─┘          └────┘  
par                                               └─┘          └────┘  
pid                                                                  
st                                             └────────────┘└─────────┘└┘
217  
218  lemma ratio_le_op_norm : ∥f x∥ / ∥x∥ ≤ ∥f∥ :=
id                                 
src                                    
typ                                
219  (or.elim (lt_or_eq_of_le (norm_nonneg _))
id    └─────┘  └────────────┘  └─────────┘
src   └─────┘  └────────────┘  └─────────┘
typ   └─────┘  └────────────┘  └─────────┘
220    (λ hlt, div_le_of_le_mul hlt (by { rw mul_comm, apply le_op_norm }))
id        └─┘  └──────────────┘ └─┘          └──────┘        └────────┘
src            └──────────────┘           └─┘└──────┘  └────┘└────────┘
typ       └─┘  └──────────────┘ └─┘       └─┘└──────┘  └────┘└────────┘
doc                                       └─┘          └────┘└────────┘
txt                                       └─┘          └────┘          
par                                       └─┘          └────┘          
pid                                                                  
st                                     └────────────┘└─────────────────┘└┘
221    (λ heq, by { rw [←heq, div_zero], apply op_norm_nonneg }))
id        └─┘            └─┘  └──────┘         └────────────┘
src       └─┘       └───┘└─┘└┘└──────┘  └────┘└────────────┘
typ       └─┘       └───┘└─┘└┘└──────┘  └────┘└────────────┘
doc                 └───┘   └┘          └────┘              
txt                 └───┘   └┘          └────┘              
par                 └───┘   └┘          └────┘              
pid                   └─┘   └┘                             
st               └─────────┘└────────┘└──────────────────────┘└┘
222  
223  /-- The image of the unit ball under a continuous linear map is bounded. -/
224  lemma unit_le_op_norm : ∥x∥ ≤ 1 → ∥f x∥ ≤ ∥f∥ :=
id                                    
src                                       
typ                                   
225  λ hx, begin
id     └┘
typ    └┘
st         └─────
226    rw [←(mul_one ∥f∥)],
id           └─────┘ 
src    └───┘ └─────┘ └┘
typ    └───┘ └─────┘└┘
doc    └───┘           └┘
txt    └───┘           └┘
par    └───┘           └┘
pid      └─┘           └┘
st   ───────────────────┘└──
227    calc _ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
id     └──┘              └────────┘
src    └──┘                └────────┘
typ    └──┘              └────────┘
doc    └──┘                 └────────┘
st   ──────────────────────────────────────
228    ...    ≤ _ : mul_le_mul_of_nonneg_left hx (op_norm_nonneg _)
id                  └───────────────────────┘ └┘  └────────────┘
src                 └───────────────────────┘     └────────────┘
typ                 └───────────────────────┘ └┘  └────────────┘
st   ─────────────────────────────────────────────────────────────┘
229  end
st   ──┘
230  
231  /-- If one controls the norm of every `A x`, then one controls the norm of `A`. -/
232  lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ∥f x∥ ≤ M * ∥x∥) :
id                                                           
src                                                                
typ                                                          
233    ∥f∥ ≤ M :=
id       
src      
typ      
234  Inf_le _ bounds_bdd_below ⟨hMp, hM⟩
id   └────┘   └──────────────┘  └─┘  └┘
src  └────┘   └──────────────┘
typ  └────┘   └──────────────┘  └─┘  └┘
235  
236  /-- The operator norm satisfies the triangle inequality. -/
237  theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
id                                  
src                                     
typ                                 
238  Inf_le _ bounds_bdd_below
id   └────┘   └──────────────┘
src  └────┘   └──────────────┘
typ  └────┘   └──────────────┘
239    ⟨add_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x, by { rw add_mul,
id      └────────┘  └────────────┘     └────────────┘                 └─────┘
src     └────────┘  └────────────┘     └────────────┘               └─┘└─────┘
typ     └────────┘  └────────────┘     └────────────┘              └─┘└─────┘
doc                                                                 └─┘
txt                                                                 └─┘
par                                                                 └─┘
pid                                                                   
st                                                               └───────────┘└─
240      exact norm_add_le_of_le (le_op_norm _ _) (le_op_norm _ _) }⟩
id             └───────────────┘                   └────────┘
src      └────┘└───────────────┘           └────┘ └────────┘└────┘
typ      └────┘└───────────────┘           └────┘ └────────┘└────┘
doc      └────┘                            └────┘ └────────┘└────┘
txt      └────┘                            └────┘           └────┘
par      └────┘                            └────┘           └────┘
pid                                       └────┘           └───┘
st   ─────────────────────────────────────────────────────────────┘└┘
241  
242  /-- An operator is zero iff its norm vanishes. -/
243  theorem op_norm_zero_iff : ∥f∥ = 0 ↔ f = 0 :=
id                                    
src                                     
typ                                   
244  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
245    (λ hn, continuous_linear_map.ext (λ x, (norm_le_zero_iff _).1
id        └┘  └───────────────────────┘       └──────────────┘   
src           └───────────────────────┘        └──────────────┘   
typ       └┘  └───────────────────────┘       └──────────────┘   
246      (calc _ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
id                      └────────┘
src                       └────────┘
typ                     └────────┘
doc                            └────────┘
247       ...     = _ : by rw [hn, zero_mul])))
id                             └┘  └──────┘
src                        └──┘  └┘└──────┘
typ                        └──┘└┘└┘└──────┘
doc                        └──┘  └┘        
txt                        └──┘  └┘        
par                        └──┘  └┘        
pid                          └┘  └┘        
st                        └─────┘└────────┘
248    (λ hf, le_antisymm (Inf_le _ bounds_bdd_below
id        └┘  └─────────┘  └────┘   └──────────────┘
src           └─────────┘  └────┘   └──────────────┘
typ       └┘  └─────────┘  └────┘   └──────────────┘
249      ⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul, hf], exact norm_zero })⟩)
id        └──────┘ └─┘      └──────┘           └──────┘  └┘         └───────┘
src       └──────┘ └─┘       └──────┘       └──┘└──────┘└┘    └────┘└───────┘
typ       └──────┘ └─┘      └──────┘       └──┘└──────┘└┘└┘  └────┘└───────┘
doc                                         └──┘        └┘    └────┘         
txt                                         └──┘        └┘    └────┘         
par                                         └──┘        └┘    └────┘         
pid                                           └┘        └┘                  
st                                       └─────────────┘└──┘└─────────────────┘└┘
250      (op_norm_nonneg _))
id        └────────────┘
src       └────────────┘
typ       └────────────┘
251  
252  @[simp] lemma norm_zero : ∥(0 : E →L[𝕜] F)∥ = 0 :=
id                                   └─┘   
src                                   └─┘     
typ                                  └─┘   
doc    └──┘                            └─┘ 
253  by rw op_norm_zero_iff
id         └──────────────┘
src     └─┘└──────────────┘
typ     └─┘└──────────────┘
doc     └─┘└──────────────┘
txt     └─┘                
par     └─┘                
pid                       
st     └────────────────────
254  
src  
typ  
doc  
txt  
par  
pid  
st   
255  /-- The norm of the identity is at most `1`. It is in fact `1`, except when the space is trivial
256  where it is `0`. It means that one can not do better than an inequality in general. -/
257  lemma norm_id : ∥(id : E →L[𝕜] E)∥ ≤ 1 :=
id                    └┘    └─┘   
src                   └┘     └─┘     
typ                   └┘    └─┘   
doc                    └┘     └─┘ 
258  op_norm_le_bound _ zero_le_one (λx, by simp)
id   └──────────────┘   └─────────┘   
src  └──────────────┘   └─────────┘         └──┘
typ  └──────────────┘   └─────────┘        └──┘
doc  └──────────────┘                       └──┘
txt                                         └──┘
par                                         └──┘
st                                         └───┘
259  
260  /-- The operator norm is homogeneous. -/
261  lemma op_norm_smul : ∥c • f∥ = ∥c∥ * ∥f∥ :=
id                              
src                                 
typ                             
262  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
263    (Inf_le _ bounds_bdd_below
id      └────┘   └──────────────┘
src     └────┘   └──────────────┘
typ     └────┘   └──────────────┘
264      ⟨mul_nonneg (norm_nonneg _) (op_norm_nonneg _), λ _,
id        └────────┘  └─────────┘     └────────────┘       
src       └────────┘  └─────────┘     └────────────┘
typ       └────────┘  └─────────┘     └────────────┘       
265      begin
st       └─────
266        erw [norm_smul, mul_assoc],
id              └───────┘  └───────┘
src        └───┘└───────┘└┘└───────┘
typ        └───┘└───────┘└┘└───────┘
doc        └───┘         └┘         
txt        └───┘         └┘         
par        └───┘         └┘         
pid           └┘         └┘         
st   ───────────────────┘└─────────┘└──
267        exact mul_le_mul_of_nonneg_left (le_op_norm _ _) (norm_nonneg _)
id               └───────────────────────┘  └────────┘       └─────────┘
src        └────┘└───────────────────────┘ └────────┘└────┘ └─────────┘└───
typ        └────┘└───────────────────────┘ └────────┘└────┘ └─────────┘└───
doc        └────┘                          └────────┘└────┘            └───
txt        └────┘                                    └────┘            └───
par        └────┘                                    └────┘            └───
pid                                                 └────┘            └─┘
st   ───────────────────────────────────────────────────────────────────────
268      end⟩)
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
269    (lb_le_Inf _ bounds_nonempty (λ _ ⟨hn, hc⟩,
id      └───────┘   └─────────────┘     
src     └───────┘   └─────────────┘
typ     └───────┘   └─────────────┘     
270      (or.elim (lt_or_eq_of_le (norm_nonneg c))
id        └─────┘  └────────────┘  └─────────┘ 
src       └─────┘  └────────────┘  └─────────┘
typ       └─────┘  └────────────┘  └─────────┘ 
271        (λ hlt,
id            └─┘
typ           └─┘
272          begin
st           └─────
273            rw mul_comm,
id                └──────┘
src            └─┘└──────┘
typ            └─┘└──────┘
doc            └─┘
txt            └─┘
par            └─┘
pid              
st   ────────────────────┘└─
274            exact mul_le_of_le_div hlt (Inf_le _ bounds_bdd_below
id                   └──────────────┘      └────┘   └──────────────┘
src            └────┘└──────────────┘    └────┘└─┘└──────────────┘
typ            └────┘└──────────────┘    └────┘└─┘└──────────────┘
doc            └────┘                          └─┘                
txt            └────┘                          └─┘                
par            └────┘                          └─┘                
pid                                           └─┘                
st   ────────────────────────────────────────────────────────────────
275            ⟨div_nonneg hn hlt, λ _,
id              └────────┘ └┘ └─┘
src  ─────────┘ └────────┘     └┘ └───
typ  ─────────┘ └────────┘└┘└─┘└┘ └───
doc  ─────────┘                └┘ └───
txt  ─────────┘                └┘ └───
par  ─────────┘                └┘ └───
pid  ─────────┘                └┘ └───
st   ───────────────────────────────────
276            (by { rw div_mul_eq_mul_div, exact le_div_of_mul_le hlt
id                      └────────────────┘        └──────────────┘ └─┘
src  ─────────┘   └─┘└─┘└────────────────┘└──────┘└──────────────┘   
typ  ─────────┘   └─┘└─┘└────────────────┘└──────┘└──────────────┘└─┘
doc  ─────────┘   └─┘└─┘                  └──────┘                   
txt  ─────────┘   └─┘└─┘                  └──────┘                   
par  ─────────┘   └─┘└─┘                  └──────┘                   
pid  ─────────┘   └────┘                  └──────┘                   
st   ────────────┘└──────────────────────┘└────────────────────────────
277            (by { rw [ mul_comm, ←norm_smul ], exact hc _ }) })⟩)
id                        └──────┘   └───────┘          └┘
src  ─────────┘   └─┘└───┘└──────┘└─┘└───────┘└┘└──────┘  └──────────
typ  ─────────┘   └─┘└───┘└──────┘└─┘└───────┘└┘└──────┘└┘└──────────
doc  ─────────┘   └─┘└───┘        └─┘         └┘└──────┘  └──────────
txt  ─────────┘   └─┘└───┘        └─┘         └┘└──────┘  └──────────
par  ─────────┘   └─┘└───┘        └─┘         └┘└──────┘  └──────────
pid  ─────────┘   └──────┘        └─┘         └────────┘  └────────┘
st   ────────────┘└──────────────┘└──────────┘└─────────────┘└┘└───
278          end)
src  ───────┘
typ  ───────┘
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘└─┘
279        (λ heq, by { rw [←heq, zero_mul], exact hn }))))
id            └─┘            └─┘  └──────┘         └┘
src           └─┘       └───┘└─┘└┘└──────┘  └────┘  
typ           └─┘       └───┘└─┘└┘└──────┘  └────┘└┘
doc                     └───┘   └┘          └────┘  
txt                     └───┘   └┘          └────┘  
par                     └───┘   └┘          └────┘  
pid                       └─┘   └┘                 
st                   └─────────┘└────────┘└──────────┘└┘
280  
281  lemma op_norm_neg : ∥-f∥ = ∥f∥ := calc
id                         
src                          
typ                        
282    ∥-f∥ = ∥(-1:𝕜) • f∥ : by rw neg_one_smul
id                       └──────────┘
src                      └─┘└──────────┘
typ                   └─┘└──────────┘
doc                             └─┘            
txt                             └─┘            
par                             └─┘            
pid                                           
st                             └────────────────
283    ... = ∥(-1:𝕜)∥ * ∥f∥ : by rw op_norm_smul
id                          └──────────┘
src  ─┘                    └─┘└──────────┘
typ  ─┘                  └─┘└──────────┘
doc  ─┘                          └─┘└──────────┘
txt  ─┘                          └─┘            
par  ─┘                          └─┘            
pid  ─┘                                        
st   ─┘                         └────────────────
284    ... = ∥f∥ : by simp
id           
src  ─┘             └────
typ  ─┘            └────
doc  ─┘               └────
txt  ─┘               └────
par  ─┘               └────
pid  ─┘                   
st   ─┘              └─────
285  
src  
typ  
doc  
txt  
par  
pid  
st   
286  /-- Continuous linear maps themselves form a normed space with respect to
287      the operator norm. -/
288  instance to_normed_group : normed_group (E →L[𝕜] F) :=
id                              └──────────┘   └─┘ 
src                             └──────────┘    └─┘ 
typ                             └──────────┘   └─┘ 
doc                             └──────────┘    └─┘ 
289  normed_group.of_core _ ⟨op_norm_zero_iff, op_norm_add_le, op_norm_neg⟩
id   └──────────────────┘    └──────────────┘  └────────────┘  └─────────┘
src  └──────────────────┘    └──────────────┘  └────────────┘  └─────────┘
typ  └──────────────────┘    └──────────────┘  └────────────┘  └─────────┘
doc  └──────────────────┘    └──────────────┘  └────────────┘
290  
291  instance to_normed_space : normed_space 𝕜 (E →L[𝕜] F) :=
id                              └──────────┘    └─┘ 
src                             └──────────┘      └─┘ 
typ                             └──────────┘    └─┘ 
doc                             └──────────┘      └─┘ 
292  ⟨op_norm_smul⟩
id    └──────────┘
src   └──────────┘
typ   └──────────┘
doc   └──────────┘
293  
294  /-- The operator norm is submultiplicative. -/
295  lemma op_norm_comp_le : ∥comp h f∥ ≤ ∥h∥ * ∥f∥ :=
id                           └──┘      
src                          └──┘          
typ                          └──┘      
doc                           └──┘
296  (Inf_le _ bounds_bdd_below
id    └────┘   └──────────────┘
src   └────┘   └──────────────┘
typ   └────┘   └──────────────┘
297    ⟨mul_nonneg (op_norm_nonneg _) (op_norm_nonneg _), λ x,
id      └────────┘  └────────────┘     └────────────┘       
src     └────────┘  └────────────┘     └────────────┘
typ     └────────┘  └────────────┘     └────────────┘       
298    begin
st     └─────
299      rw mul_assoc,
id          └───────┘
src      └─┘└───────┘
typ      └─┘└───────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───────────────┘└─
300      calc _ ≤ ∥h∥ * ∥f x∥: le_op_norm _ _
id       └──┘         
src      └──┘       
typ      └──┘         
doc      └──┘
st   ─────────────────────────────────────────
301      ... ≤ _ : mul_le_mul_of_nonneg_left
id                 └───────────────────────┘
src                └───────────────────────┘
typ                └───────────────────────┘
st   ────────────────────────────────────────
302                (le_op_norm _ _) (op_norm_nonneg _)
id                  └────────┘       └────────────┘
src                 └────────┘       └────────────┘
typ                 └────────┘       └────────────┘
doc                 └────────┘
st   ────────────────────────────────────────────────┘
303    end⟩)
st   ────┘
304  
305  /-- continuous linear maps are Lipschitz continuous. -/
306  theorem lipschitz : lipschitz_with ⟨∥f∥, op_norm_nonneg f⟩ f :=
id                       └────────────┘    └────────────┘   
src                      └────────────┘     └────────────┘
typ                      └────────────┘    └────────────┘   
doc                      └────────────┘
307  λ x y, by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }
id                 └──────────┘  └──────────┘   └─────┘         └────────┘
src              └──┘└──────────┘└┘└──────────┘└─┘└─────┘  └────┘└────────┘
typ            └──┘└──────────┘└┘└──────────┘└─┘└─────┘  └────┘└────────┘
doc              └──┘            └┘            └─┘         └────┘└────────┘
txt              └──┘            └┘            └─┘         └────┘          
par              └──┘            └┘            └─┘         └────┘          
pid                └┘            └┘            └─┘                        
st            └─────────────────┘└────────────┘└────────┘└──────────────────┘└┘
308  
309  /-- A continuous linear map is automatically uniformly continuous. -/
310  protected theorem uniform_continuous : uniform_continuous f :=
id                                          └────────────────┘ 
src                                         └────────────────┘
typ                                         └────────────────┘ 
311  f.lipschitz.to_uniform_continuous
id   └────────┘└────────────────────┘
src   └────────┘└────────────────────┘
typ  └────────┘└────────────────────┘
doc   └────────┘└────────────────────┘
312  
313  variable {f}
314  /-- A continuous linear map is an isometry if and only if it preserves the norm. -/
315  lemma isometry_iff_norm_image_eq_norm :
316    isometry f ↔ ∀x, ∥f x∥ = ∥x∥ :=
id     └──────┘         
src    └──────┘              
typ    └──────┘         
doc    └──────┘
317  begin
st   └─────
318    rw isometry_emetric_iff_metric,
id        └─────────────────────────┘
src    └─┘└─────────────────────────┘
typ    └─┘└─────────────────────────┘
doc    └─┘└─────────────────────────┘
txt    └─┘
par    └─┘
pid      
st   ───────────────────────────────┘└─
319    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
320    { assume H x,
src      └────────┘
typ      └────────┘
doc      └────────┘
txt      └────────┘
par      └────────┘
pid      └────────┘
st   ───┘└────────┘└─
321      have := H x 0,
id                
src      └──────┘  └┘
typ      └──────┘└┘
doc      └──────┘  └┘
txt      └──────┘  └┘
par      └──────┘  └┘
pid      └───┘└─┘  
st   ────────────────┘└─
322      rwa [dist_eq_norm, dist_eq_norm, f.map_zero, sub_zero, sub_zero] at this },
id            └──────────┘  └──────────┘              └──────┘  └──────┘
src      └───┘└──────────┘└┘└──────────┘└┘          └┘└──────┘└┘└──────┘└────────┘
typ      └───┘└──────────┘└┘└──────────┘└┘└────────┘└┘└──────┘└┘└──────┘└────────┘
doc      └───┘            └┘            └┘          └┘        └┘        └────────┘
txt      └───┘            └┘            └┘          └┘        └┘        └────────┘
par      └───┘            └┘            └┘          └┘        └┘        └────────┘
pid         └┘            └┘            └┘          └┘        └┘        └──────┘
st   ────────────────────┘└────────────┘└──────────┘└────────┘└────────┘└───────┘└┘
323    { assume H x y,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───────────────┘└─
324      rw [dist_eq_norm, dist_eq_norm, ← f.map_sub, H] }
id           └──────────┘  └──────────┘               
src      └──┘└──────────┘└┘└──────────┘└──┘         └┘ └┘
typ      └──┘└──────────┘└┘└──────────┘└──┘└───────┘└┘└┘
doc      └──┘            └┘            └──┘         └┘ └┘
txt      └──┘            └┘            └──┘         └┘ └┘
par      └──┘            └┘            └──┘         └┘ └┘
pid        └┘            └┘            └──┘         └┘ 
st   ───────────────────┘└────────────┘└───────────┘└─┘└─
325  end
st   ──┘
326  
327  variable (f)
328  /-- A continuous linear map is a uniform embedding if it expands the norm by a constant factor. -/
329  theorem uniform_embedding_of_bound (C : ℝ) (hC : ∀x, ∥x∥ ≤ C * ∥f x∥) :
id                                                           
src                                                               
typ                                                          
330    uniform_embedding f :=
id     └───────────────┘ 
src    └───────────────┘
typ    └───────────────┘ 
331  begin
st   └─────
332    have Cpos : 0 < max C 1 := lt_of_lt_of_le zero_lt_one (le_max_right _ _),
id                    └─┘       └────────────┘ └─────────┘  └──────────┘
src    └────────────┘└─┘ └────┘└────────────┘└─────────┘ └──────────┘└───┘
typ    └────────────┘└─┘└────┘└────────────┘└─────────┘ └──────────┘└───┘
doc    └────────────┘     └────┘                                      └───┘
txt    └────────────┘     └────┘                                      └───┘
par    └────────────┘     └────┘                                      └───┘
pid    └───────┘└───┘     └───┘                                      └───┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
333    refine uniform_embedding_iff'.2 ⟨metric.uniform_continuous_iff.1 f.uniform_continuous,
id            └────────────────────┘    └───────────────────────────┘   └──────────────────┘
src    └─────┘└────────────────────┘└─┘ └───────────────────────────┘└─┘└──────────────────┘└─
typ    └─────┘└────────────────────┘└─┘ └───────────────────────────┘└─┘└──────────────────┘└─
doc    └─────┘└────────────────────┘└─┘                              └─┘└──────────────────┘└─
txt    └─────┘                      └─┘                              └─┘                    └─
par    └─────┘                      └─┘                              └─┘                    └─
pid                                └─┘                              └─┘                    └─
st   ─────────────────────────────────────────────────────────────────────────────────────────
334                                      λδ δpos, ⟨δ / (max C 1), div_pos δpos Cpos, λx y hxy, _⟩⟩,
id                                                     └─┘      └─────┘      └──┘
src  ───────────────────────────────────┘ └──────┘   └─┘ └───┘└─────┘        └┘ └──────────┘
typ  ───────────────────────────────────┘ └──────┘   └─┘└───┘└─────┘    └──┘└┘ └──────────┘
doc  ───────────────────────────────────┘ └──────┘        └───┘               └┘ └──────────┘
txt  ───────────────────────────────────┘ └──────┘        └───┘               └┘ └──────────┘
par  ───────────────────────────────────┘ └──────┘        └───┘               └┘ └──────────┘
pid  ───────────────────────────────────┘ └──────┘        └───┘               └┘ └──────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
335    calc dist x y = ∥x - y∥ : by rw dist_eq_norm
id     └──┘                          └──────────┘
src    └──┘                         └─┘└──────────┘
typ    └──┘                       └─┘└──────────┘
doc    └──┘                         └─┘            
txt                                 └─┘            
par                                 └─┘            
pid                                               
st   ─────────────────────────────┘└────────────────
336    ... ≤ C * ∥f (x - y)∥ : hC _
id                        └┘
src  ─┘                  
typ  ─┘                   └┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└────────────────────────────
337    ... = C * dist (f x) (f y) : by rw [f.map_sub, dist_eq_norm]
id               └──┘                                 └──────────┘
src              └──┘                  └──┘         └┘└──────────┘└─
typ              └──┘                  └──┘└───────┘└┘└──────────┘└─
doc                                    └──┘         └┘            └─
txt                                    └──┘         └┘            └─
par                                    └──┘         └┘            └─
pid                                      └┘         └┘            
st   ────────────────────────────────┘└────────────┘└────────────┘
338    ... ≤ max C 1 * dist (f x) (f y) :
id           └─┘
src  ─┘      └─┘
typ  ─┘      └─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└──────────────────────────────────
339      mul_le_mul_of_nonneg_right (le_max_left _ _) dist_nonneg
id       └────────────────────────┘  └─────────┘      └─────────┘
src      └────────────────────────┘  └─────────┘      └─────────┘
typ      └────────────────────────┘  └─────────┘      └─────────┘
st   ─────────────────────────────────────────────────────────────
340    ... < max C 1 * (δ / max C 1) : mul_lt_mul_of_pos_left hxy Cpos
id                                    └────────────────────┘ └─┘ └──┘
src                                   └────────────────────┘
typ                                   └────────────────────┘ └─┘ └──┘
st   ──────────────────────────────────────────────────────────────────
341    ... = δ : by { rw mul_comm, exact div_mul_cancel _ (ne_of_lt Cpos).symm }
id                      └──────┘        └────────────┘    └──────┘ └──┘
src                   └─┘└──────┘  └────┘└────────────┘└─┘ └──────┘    └─────┘
typ                  └─┘└──────┘  └────┘└────────────┘└─┘ └──────┘└──┘└─────┘
doc                   └─┘          └────┘              └─┘             └─────┘
txt                   └─┘          └────┘              └─┘             └─────┘
par                   └─┘          └────┘              └─┘             └─────┘
pid                                                  └─┘             └───┘└┘
st   ─────────────┘└────────────┘└────────────────────────────────────────────┘└─
342  end
st   ──┘
343  
344  /-- If a continuous linear map is a uniform embedding, then it expands the norm by a positive
345  factor.-/
346  theorem bound_of_uniform_embedding (hf : uniform_embedding f) :
id                                            └───────────────┘ 
src                                           └───────────────┘
typ                                           └───────────────┘ 
347    ∃ C : ℝ, 0 < C ∧ ∀x, ∥x∥ ≤ C * ∥f x∥ :=
id                        
src                             
typ                       
348  begin
st   └─────
349    obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ) (H : ε > 0), ∀ {x y : E}, dist (f x) (f y) < ε → dist x y < 1, from
id                                                                                 └──┘
src    └─────────────────────┘└────┘ └─────┘ └─┘ └──────┘         └┘   └┘  └──┘   └┘  └────
typ    └─────────────────────┘└────┘ └─────┘ └─┘ └──────┘        └┘  └┘  └──┘   └┘  └────
doc    └─────────────────────┘ └────┘ └─────┘  └─┘  └──────┘         └┘   └┘          └┘  └────
txt    └─────────────────────┘ └────┘ └─────┘  └─┘  └──────┘         └┘   └┘          └┘  └────
par    └─────────────────────┘ └────┘ └─────┘  └─┘  └──────┘         └┘   └┘          └┘  └────
pid          └───────────────┘ └────┘ └─────┘  └─┘  └──────┘         └┘   └┘            └────
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└──────
350      (uniform_embedding_iff.1 hf).2.2 1 zero_lt_one,
id        └───────────────────┘   └┘        └─────────┘
src  ───┘ └───────────────────┘└─┘  └──────┘└─────────┘
typ  ───┘ └───────────────────┘└─┘└┘└──────┘└─────────┘
doc  ───┘                      └─┘  └──────┘
txt  ───┘                      └─┘  └──────┘
par  ───┘                      └─┘  └──────┘
pid  ───┘                      └─┘  └──────┘
st   ─────────────────────────────────────────────────┘└─
351    let δ := ε/2,
id              
src    └───────┘ 
typ    └───────┘
doc    └───────┘  
txt    └───────┘  
par    └───────┘  
pid    └───┘└─┘  
st   ─────────────┘└─
352    have δ_pos : δ > 0 := half_pos εpos,
id                          └──────┘ └──┘
src    └───────────┘  └────┘└──────┘
typ    └───────────┘ └────┘└──────┘└──┘
doc    └───────────┘  └────┘        
txt    └───────────┘  └────┘        
par    └───────────┘  └────┘        
pid    └────────┘└─┘  └───┘        
st   ────────────────────────────────────┘└─
353    have H : ∀{x}, ∥f x∥ ≤ δ → ∥x∥ ≤ 1,
id                        
src    └───────┘ └─┘         └┘
typ    └───────┘ └─┘       └┘
doc    └───────┘ └─┘            └┘
txt    └───────┘ └─┘            └┘
par    └───────┘ └─┘            └┘
pid    └────┘└─┘ └─┘            
st   ───────────────────────────────────┘└─
354    { assume x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid      └─────────┘
st   ───┘└─────────┘└─
355      have : dist x 0 ≤ 1,
id              └──┘ 
src      └─────┘└──┘ └─┘ └┘
typ      └─────┘└──┘└─┘ └┘
doc      └─────┘     └─┘ └┘
txt      └─────┘     └─┘ └┘
par      └─────┘     └─┘ └┘
pid      └───┘└┘     └─┘ 
st   ──────────────────────┘└─
356      { apply le_of_lt,
id               └──────┘
src        └────┘└──────┘
typ        └────┘└──────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└────────────┘└─
357        apply hε,
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────────────┘└─
358        simp [dist_eq_norm],
id               └──────────┘
src        └────┘└──────────┘
typ        └────┘└──────────┘
doc        └────┘            
txt        └────┘            
par        └────┘            
pid                        
st   ────────────────────────┘└─
359        exact lt_of_le_of_lt hx (half_lt_self εpos) },
id               └────────────┘ └┘  └──────────┘ └──┘
src        └────┘└────────────┘   └──────────┘    └┘
typ        └────┘└────────────┘└┘ └──────────┘└──┘└┘
doc        └────┘                                 └┘
txt        └────┘                                 └┘
par        └────┘                                 └┘
pid                                              
st   ─────────────────────────────────────────────────┘└┘
360    simpa using this },
id                 └──┘
src    └──────────┘    
typ    └──────────┘└──┘
doc    └──────────┘    
txt    └──────────┘    
par    └──────────┘    
pid         └────┘    
st   ──────────────────┘└┘
361    rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
id            └─────────────────────────────┘ 
src    └─────┘└─────────────────────────────┘ └───────────┘
typ    └─────┘└─────────────────────────────┘└───────────┘
doc    └─────┘                                └───────────┘
txt    └─────┘                                └───────────┘
par    └─────┘                                └───────────┘
pid                                          └───────────┘
st   ──────────────────────────────────────────────────────┘└─
362    refine ⟨δ⁻¹ * ∥c∥, (mul_pos (inv_pos δ_pos) ((lt_trans zero_lt_one hc))), (λx, _)⟩,
id             └┘       └─────┘  └─────┘ └───┘    └──────┘ └─────────┘ └┘
src    └─────┘  └┘   └┘ └─────┘ └─────┘     └┘  └──────┘└─────────┘  └───┘  └────┘
typ    └─────┘ └┘  └┘ └─────┘ └─────┘└───┘└┘  └──────┘└─────────┘└┘└───┘  └────┘
doc    └─────┘        └┘                     └┘                       └───┘  └────┘
txt    └─────┘        └┘                     └┘                       └───┘  └────┘
par    └─────┘        └┘                     └┘                       └───┘  └────┘
pid                  └┘                     └┘                       └───┘  └────┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
363    by_cases hx : f x = 0,
id                     
src    └───────┘  └─┘  └┘
typ    └───────┘  └─┘└┘
doc    └───────┘  └─┘   └┘
txt    └───────┘  └─┘   └┘
par    └───────┘  └─┘   └┘
pid              └─┘   
st   ──────────────────────┘└─
364    { have : f x = f 0, by { simp [hx] },
id                   
src      └─────┘    └┘
typ      └─────┘  └┘
doc      └─────┘    └┘
txt      └─────┘    └┘
par      └─────┘    └┘
pid      └───┘└┘    
st   ───┘└──────────────┘                 └┘
365      have : x = 0 := (uniform_embedding_iff.1 hf).1 this,
id              
typ             
366      simp [this] },
st                   └┘
367    { rcases rescale_to_shell hc δ_pos hx with ⟨d, hd, dxle, ledx, dinv⟩,
368      have : ∥f (d • x)∥ ≤ δ, by simpa,
id                          
typ                         
369      have : ∥d • x∥ ≤ 1 := H this,
id                  
typ                 
370      calc ∥x∥ = ∥d∥⁻¹ * ∥d • x∥ :
id                              
typ                             
371        by rwa [← normed_field.norm_inv, ← norm_smul, ← mul_smul, inv_mul_cancel, one_smul]
372      ... ≤ ∥d∥⁻¹ * 1 :
373        mul_le_mul_of_nonneg_left this (inv_nonneg.2 (norm_nonneg _))
374      ... ≤ δ⁻¹ * ∥c∥ * ∥f x∥ :
id                   
typ                  
375        by rwa [mul_one] }
st                          └─
376  end
st   ──┘
377  
378  section uniformly_extend
379  
380  variables [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e)
381  
382  section
383  variables (h_e : uniform_inducing e)
384  
385  /-- Extension of a continuous linear map `f : E →L[𝕜] F`, with `E` a normed space and `F` a complete
386      normed space, along a uniform and dense embedding `e : E →L[𝕜] G`.  -/
387  def extend : G →L[𝕜] F :=
id                      
typ                     
388  /- extension of `f` is continuous -/
389  have cont : _ := (uniform_continuous_uniformly_extend h_e h_dense f.uniform_continuous).continuous,
390  /- extension of `f` agrees with `f` on the domain of the embedding `e` -/
391  have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous,
392  { to_fun := (h_e.dense_inducing h_dense).extend f,
393    add :=
394    begin
395      refine is_closed_property2 h_dense (is_closed_eq _ _) _,
396      { exact cont.comp (continuous_fst.add continuous_snd) },
st                                                             └┘
397      { exact (cont.comp continuous_fst).add (cont.comp continuous_snd) },
st                                                                         └┘
398      { assume x y, rw ← e.map_add, simp only [eq], exact f.map_add _ _  },
st                                                                          └┘
399    end,
st     └─┘
400    smul := λk,
id              
typ             
401    begin
402      refine is_closed_property h_dense (is_closed_eq _ _) _,
403      { exact cont.comp (continuous_const.smul continuous_id)  },
st                                                                └┘
404      { exact (continuous_const.smul continuous_id).comp cont },
st                                                               └┘
405      { assume x, rw ← map_smul, simp only [eq], exact map_smul _ _ _  },
st                                                                        └┘
406    end,
st     └─┘
407    cont := cont
408  }
409  
410  @[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) e h_dense h_e = 0 :=
id                                                 
typ                                                
doc    └──┘
411  begin
412    apply ext,
413    refine is_closed_property h_dense (is_closed_eq _ _) _,
414    { exact (uniform_continuous_uniformly_extend h_e h_dense uniform_continuous_const).continuous },
st                                                                                                   └┘
415    { simp only [zero_apply], exact continuous_const },
st                                                      └┘
416    { assume x, exact uniformly_extend_of_ind h_e h_dense uniform_continuous_const x }
id                                                                                    
typ                                                                                   
st                                                                                      └─
417  end
st   ──┘
418  
419  end
420  
421  section
422  variables {N : ℝ} (h_e : ∀x, ∥x∥ ≤ N * ∥e x∥)
id                                          
src                 
typ                                         
423  
424  local notation `ψ` := f.extend e h_dense (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing
425  
426  /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the norm
427      of the extension of `f` along `e` is bounded by `N * ∥f∥`. -/
428  lemma op_norm_extend_le : ∥ψ∥ ≤ N * ∥f∥ :=
id                                   
typ                                  
429  begin
430    have uni : uniform_inducing e := (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing,
431    have eq : ∀x, ψ (e x) = f x := uniformly_extend_of_ind uni h_dense f.uniform_continuous,
id                
typ               
432    by_cases N0 : 0 ≤ N,
id                       
typ                      
433    { refine op_norm_le_bound ψ _ (is_closed_property h_dense (is_closed_le _ _) _),
434      { exact mul_nonneg N0 (norm_nonneg _) },
st                                             └┘
435      { exact continuous_norm.comp (cont ψ) },
st                                             └┘
436      { exact continuous_const.mul continuous_norm },
st                                                    └┘
437      { assume x,
438        rw eq,
439        calc ∥f x∥ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _
440          ... ≤ ∥f∥ * (N * ∥e x∥) : mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _)
id                                                                    
typ                                                                   
441          ... ≤ N * ∥f∥ * ∥e x∥ : by rw [mul_comm N ∥f∥, mul_assoc] } },
id                                                  
typ                                                 
st                                                                    └──┘
442    { have he : ∀ x : E, x = 0,
id                       
typ                      
443      { assume x,
444        have N0 : N ≤ 0 := le_of_lt (lt_of_not_ge N0),
id                   
typ                  
445        rw ← norm_le_zero_iff,
446        exact le_trans (h_e x) (mul_nonpos_of_nonpos_of_nonneg N0 (norm_nonneg _)) },
id                             
typ                            
st                                                                                    └┘
447      have hf : f = 0, { ext, simp only [he x, zero_apply, map_zero] },
id                                             
typ                                            
st                                                                      └┘
448      have hψ : ψ = 0, { rw hf, apply extend_zero },
st                                                   └┘
449      rw [hψ, hf, norm_zero, norm_zero, mul_zero] }
st                                                  └─
450  end
st   ──┘
451  
452  end
453  
454  end uniformly_extend
455  
456  end op_norm
457  
458  /-- The norm of the tensor product of a scalar linear map and of an element of a normed space
459  is the product of the norms. -/
460  @[simp] lemma smul_right_norm {c : E →L[𝕜] 𝕜} {f : F} :
id                                                   
typ                                                  
doc    └──┘
461    ∥smul_right c f∥ = ∥c∥ * ∥f∥ :=
id                              
typ                             
462  begin
463    refine le_antisymm _ _,
464    { apply op_norm_le_bound _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) (λx, _),
id                                                                               
typ                                                                              
465      calc
466       ∥(c x) • f∥ = ∥c x∥ * ∥f∥ : norm_smul _ _
id                              
typ                             
467       ... ≤ (∥c∥ * ∥x∥) * ∥f∥ :
468         mul_le_mul_of_nonneg_right (le_op_norm _ _) (norm_nonneg _)
469       ... = ∥c∥ * ∥f∥ * ∥x∥ : by ring },
st                                        └┘
470    { by_cases h : ∥f∥ = 0,
id                     
typ                    
471      { rw h, simp [norm_nonneg] },
st                                  └┘
472      { have : 0 < ∥f∥ := lt_of_le_of_ne (norm_nonneg _) (ne.symm h),
id                     
typ                    
473        rw ← le_div_iff this,
474        apply op_norm_le_bound _ (div_nonneg (norm_nonneg _) this) (λx, _),
id                                                                      
typ                                                                     
475        rw [div_mul_eq_mul_div, le_div_iff this],
476        calc ∥c x∥ * ∥f∥ = ∥c x • f∥ : (norm_smul _ _).symm
id                                  
typ                                 
477        ... = ∥((smul_right c f) : E → F) x∥ : rfl
id                                       
typ                                      
478        ... ≤ ∥smul_right c f∥ * ∥x∥ : le_op_norm _ _ } },
st                                                       └──┘
479  end
st   └─┘
480  
481  section restrict_scalars
482  
483  variable (𝕜)
484  variables {𝕜' : Type*} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
id                           └──────────┘
src                          └──────────┘
typ                          └──────────┘
doc                          └──────────┘
485  {E' : Type*} [normed_group E'] [normed_space 𝕜' E']
id                 └──────────┘
src                └──────────┘
typ                └──────────┘
doc                └──────────┘
486  {F' : Type*} [normed_group F'] [normed_space 𝕜' F']
id                 └──────────┘
src                └──────────┘
typ                └──────────┘
doc                └──────────┘
487  
488  local attribute [instance, priority 500] normed_space.restrict_scalars
id                                            └───────────────────────────┘
src                                           └───────────────────────────┘
typ                                           └───────────────────────────┘
doc                                           └───────────────────────────┘
489  
490  /-- `𝕜`-linear continuous function induced by a `𝕜'`-linear continuous function when `𝕜'` is a
491  normed algebra over `𝕜`. -/
492  def restrict_scalars (f : E' →L[𝕜'] F') : E' →L[𝕜] F' :=
id                             └┘ └─┘└┘ └┘    └┘ └─┘ └┘
src                               └─┘            └─┘ 
typ                            └┘ └─┘└┘ └┘    └┘ └─┘ └┘
doc                               └─┘            └─┘ 
493  { cont := f.cont,
id             └───┘
src             └───┘
typ            └───┘
494    ..linear_map.restrict_scalars 𝕜 (f.to_linear_map) }
id       └─────────────────────────┘   └────────────┘
src      └─────────────────────────┘     └────────────┘
typ      └─────────────────────────┘   └────────────┘
doc      └─────────────────────────┘
495  
496  @[simp, move_cast] lemma restrict_scalars_coe_eq_coe (f : E' →L[𝕜'] F') :
id                                                             └┘ └─┘└┘ └┘
src                                                               └─┘  
typ                                                            └┘ └─┘└┘ └┘
doc    └──┘  └───────┘                                            └─┘  
497    (f.restrict_scalars 𝕜 : E' →ₗ[𝕜] F') = (f : E' →ₗ[𝕜'] F').restrict_scalars 𝕜 := rfl
id      └───────────────┘    └┘ └─┘ └┘       └┘ └─┘└┘ └┘ └──────────────┘      └─┘
src      └───────────────┘        └─┘               └─┘      └──────────────┘       └─┘
typ     └───────────────┘    └┘ └─┘ └┘       └┘ └─┘└┘ └┘ └──────────────┘      └─┘
doc      └───────────────┘                                      └──────────────┘
498  
499  @[simp, squash_cast] lemma restrict_scalars_coe_eq_coe' (f : E' →L[𝕜'] F') :
id                                                                └┘ └─┘└┘ └┘
src                                                                  └─┘  
typ                                                               └┘ └─┘└┘ └┘
doc    └──┘  └─────────┘                                             └─┘  
500    (f.restrict_scalars 𝕜 : E' → F') = f := rfl
id      └───────────────┘    └┘   └┘       └─┘
src      └───────────────┘                    └─┘
typ     └───────────────┘    └┘   └┘       └─┘
doc      └───────────────┘
501  
502  end restrict_scalars
503  
504  end continuous_linear_map
505  
506  /-- If both directions in a linear equiv `e` are continuous, then `e` is a uniform embedding. -/
507  lemma linear_equiv.uniform_embedding (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous e.symm) :
id                                              └─┘         └────────┘         └────────┘ └───┘
src                                              └─┘           └────────┘          └────────┘  └───┘
typ                                             └─┘         └────────┘         └────────┘ └───┘
doc                                              └─┘           └────────┘          └────────┘  └───┘
508    uniform_embedding e :=
id     └───────────────┘ 
src    └───────────────┘
typ    └───────────────┘ 
509  begin
510    rcases linear_map.bound_of_continuous e.symm.to_linear_map h₂ with ⟨C, Cpos, hC⟩,
511    let f : E →L[𝕜] F := { cont := h₁, ..e },
512    apply f.uniform_embedding_of_bound C (λx, _),
513    have : e.symm (e x) = x := linear_equiv.symm_apply_apply _ _,
514    conv_lhs { rw ← this },
515    exact hC _
516  end
st   └─┘
517  
518  /-- If a continuous linear map is constructed from a linear map via the constructor `mk_continuous`,
519  then its norm is bounded by the bound given to the constructor if it is nonnegative. -/
520  lemma linear_map.mk_continuous_norm_le (f : E →ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
id                                                └─┘                                  
src                                                └─┘                                          
typ                                               └─┘                                  
521    ∥f.mk_continuous C h∥ ≤ C :=
id     └────────────┘    
src     └────────────┘     
typ    └────────────┘    
doc      └────────────┘
522  continuous_linear_map.op_norm_le_bound _ hC h